Nuprl Lemma : R-possible_wf
11,40
postcript
pdf
R
:es_realizer{i:l},
es
:ES{i}. R-possible{i:l}(
R
;
es
)
{i'}
latex
Definitions
P
&
Q
,
x
:
A
.
B
(
x
)
,
A
c
B
,
Possible(
R
;
es
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
es
realizer
wf
,
w-es
wf
,
event
system
wf
,
R-Dsys
wf
,
possible-world
wf
,
fair-fifo
wf
,
world
wf
,
R-Feasible
wf
origin
R:es_realizer{i:l}, es:ES{i}. R-possible{i:l}(R; es) 
{i'} R:es_realizer{i:l}, es:ES{i}. R-possible{i:l}(R; es) {i'} 
x:A. B(x)
B Tx:A. B(x)
Q